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

proof

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;

then A4: the point-map of F1 = the point-map of F2 by FUNCT_2:12;
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

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;

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