let f1, f2 be Assign of (BASSModel (R,BASSIGN)); :: thesis: ( ( 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 ; :: thesis: f1 = f2
for s being object st s in S holds
(Fid (f1,S)) . s = (Fid (f2,S)) . s

proof

let s be object ; :: thesis: ( s in S implies (Fid (f1,S)) . s = (Fid (f2,S)) . s )
assume A6: s in S ; :: thesis: (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 ; :: thesis: verum

end;

hence f1 = f2 by Lm42, FUNCT_2:12; :: thesis: verum