let f1, f2 be strict IncProjMap over 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 that
A18: for A being POINT of (G_ (k,X)) holds f1 . A = s .: A and
A19: for L being LINE of (G_ (k,X)) holds f1 . L = s .: L and
A20: for A being POINT of (G_ (k,X)) holds f2 . A = s .: A and
A21: for L being LINE of (G_ (k,X)) holds f2 . L = s .: L ; :: thesis: f1 = f2
A22: 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 by A19;
hence f1 . L = f2 . L by A21; :: thesis: verum
end;
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 by A18;
hence f1 . A = f2 . A by A20; :: thesis: verum
end;
hence f1 = f2 by A22, Th16; :: thesis: verum