let S1, S2 be IncProjStr ; :: thesis: for F1, F2 being IncProjMap over S1,S2 st ( for A being POINT of S1 holds F1 . A = F2 . A ) & ( for L being LINE of S1 holds F1 . L = F2 . L ) holds

IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #)

let F1, F2 be IncProjMap over S1,S2; :: thesis: ( ( for A being POINT of S1 holds F1 . A = F2 . A ) & ( for L being LINE of S1 holds F1 . L = F2 . L ) implies IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #) )

assume that

A1: for A being POINT of S1 holds F1 . A = F2 . A and

A2: for L being LINE of S1 holds F1 . L = F2 . L ; :: thesis: IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #)

for a being object st a in the Points of S1 holds

the point-map of F1 . a = the point-map of F2 . a

for l being object st l in the Lines of S1 holds

the line-map of F1 . l = the line-map of F2 . l

IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #)

let F1, F2 be IncProjMap over S1,S2; :: thesis: ( ( for A being POINT of S1 holds F1 . A = F2 . A ) & ( for L being LINE of S1 holds F1 . L = F2 . L ) implies IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #) )

assume that

A1: for A being POINT of S1 holds F1 . A = F2 . A and

A2: for L being LINE of S1 holds F1 . L = F2 . L ; :: thesis: IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #)

for a being object st a in the Points of S1 holds

the point-map of F1 . a = the point-map of F2 . a

proof

then A4:
the point-map of F1 = the point-map of F2
by FUNCT_2:12;
let a be object ; :: thesis: ( a in the Points of S1 implies the point-map of F1 . a = the point-map of F2 . a )

assume a in the Points of S1 ; :: thesis: the point-map of F1 . a = the point-map of F2 . a

then consider A being POINT of S1 such that

A3: A = a ;

F1 . A = F2 . A by A1;

hence the point-map of F1 . a = the point-map of F2 . a by A3; :: thesis: verum

end;assume a in the Points of S1 ; :: thesis: the point-map of F1 . a = the point-map of F2 . a

then consider A being POINT of S1 such that

A3: A = a ;

F1 . A = F2 . A by A1;

hence the point-map of F1 . a = the point-map of F2 . a by A3; :: thesis: verum

for l being object st l in the Lines of S1 holds

the line-map of F1 . l = the line-map of F2 . l

proof

hence
IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #)
by A4, FUNCT_2:12; :: thesis: verum
let l be object ; :: thesis: ( l in the Lines of S1 implies the line-map of F1 . l = the line-map of F2 . l )

assume l in the Lines of S1 ; :: thesis: the line-map of F1 . l = the line-map of F2 . l

then consider L being LINE of S1 such that

A5: L = l ;

F1 . L = F2 . L by A2;

hence the line-map of F1 . l = the line-map of F2 . l by A5; :: thesis: verum

end;assume l in the Lines of S1 ; :: thesis: the line-map of F1 . l = the line-map of F2 . l

then consider L being LINE of S1 such that

A5: L = l ;

F1 . L = F2 . L by A2;

hence the line-map of F1 . l = the line-map of F2 . l by A5; :: thesis: verum