let f1, f2 be Assign of (BASSModel (R,BASSIGN)); ( ( for s being set st s in S holds
(Fid (f1,S)) . s = (chi (T,S)) . s ) & ( for s being set st s in S holds
(Fid (f2,S)) . s = (chi (T,S)) . s ) implies f1 = f2 )
assume that
A4:
for s being set st s in S holds
(Fid (f1,S)) . s = (chi (T,S)) . s
and
A5:
for s being set st s in S holds
(Fid (f2,S)) . s = (chi (T,S)) . s
; f1 = f2
for s being object st s in S holds
(Fid (f1,S)) . s = (Fid (f2,S)) . s
proof
let s be
object ;
( s in S implies (Fid (f1,S)) . s = (Fid (f2,S)) . s )
assume A6:
s in S
;
(Fid (f1,S)) . s = (Fid (f2,S)) . s
(Fid (f1,S)) . s =
(chi (T,S)) . s
by A4, A6
.=
(Fid (f2,S)) . s
by A5, A6
;
hence
(Fid (f1,S)) . s = (Fid (f2,S)) . s
;
verum
end;
hence
f1 = f2
by Lm42, FUNCT_2:12; verum