let f1, f2 be strict IncProjMap of G_ k,X, G_ k,X; :: thesis: ( ( for A being POINT of (G_ k,X) holds f1 . A = s .: A ) & ( for L being LINE of (G_ k,X) holds f1 . L = s .: L ) & ( for A being POINT of (G_ k,X) holds f2 . A = s .: A ) & ( for L being LINE of (G_ k,X) holds f2 . L = s .: L ) implies f1 = f2 )
assume A18: ( ( for A being POINT of (G_ k,X) holds f1 . A = s .: A ) & ( for L being LINE of (G_ k,X) holds f1 . L = s .: L ) & ( for A being POINT of (G_ k,X) holds f2 . A = s .: A ) & ( for L being LINE of (G_ k,X) holds f2 . L = s .: L ) ) ; :: thesis: f1 = f2
A19: for A being POINT of (G_ k,X) holds f1 . A = f2 . A

proof

let A be POINT of (G_ k,X); :: thesis: f1 . A = f2 . A
( f1 . A = s .: A & f2 . A = s .: A ) by A18;
hence f1 . A = f2 . A ; :: thesis: verum

end;

for L being LINE of (G_ k,X) holds f1 . L = f2 . L

proof

let L be LINE of (G_ k,X); :: thesis: f1 . L = f2 . L
( f1 . L = s .: L & f2 . L = s .: L ) by A18;
hence f1 . L = f2 . L ; :: thesis: verum

end;

hence f1 = f2 by A19, Th16; :: thesis: verum