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

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

for A being POINT of (G_ (k,X)) holds f1 . A = f2 . A
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;f1 . L = s .: L by A19;

hence f1 . L = f2 . L by A21; :: thesis: verum

proof

hence
f1 = f2
by A22, Th16; :: thesis: verum
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;f1 . A = s .: A by A18;

hence f1 . A = f2 . A by A20; :: thesis: verum