let f1, f2 be Assign of (CTLModel 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 set st s in S holds
(Fid f1,S) . s = (Fid f2,S) . s

proof

let s be set ; :: 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 Lm48, FUNCT_2:18; :: thesis: verum