let S1, S2 be IncProjStr ; :: thesis: for F1, F2 being IncProjMap of 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 of 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 A1: ( ( for A being POINT of S1 holds F1 . A = F2 . A ) & ( 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 #)
A2: for a being set st a in the Points of S1 holds
the point-map of F1 . a = the point-map of F2 . a

proof

let a be set ; :: 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;

for l being set st l in the Lines of S1 holds
the line-map of F1 . l = the line-map of F2 . l

proof

let l be set ; :: 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
A4: L = l ;
F1 . L = F2 . L by A1;
hence the line-map of F1 . l = the line-map of F2 . l by A4; :: thesis: verum

end;

then ( the point-map of F1 = the point-map of F2 & the line-map of F1 = the line-map of F2 ) by A2, FUNCT_2:18;
hence IncProjMap(# the point-map of F1,the line-map of F1 #) = IncProjMap(# the point-map of F2,the line-map of F2 #) ; :: thesis: verum