let F1, F2 be V217() Function of bool S, bool S; :: thesis: ( ( for G being Subset of holds F1 . G = SigFaxTau f,G,R,BASSIGN ) & ( for G being Subset of holds F2 . G = SigFaxTau f,G,R,BASSIGN ) implies F1 = F2 )
assume that
A6: for G being Subset of holds F1 . G = SigFaxTau f,G,R,BASSIGN and
A7: for G being Subset of holds F2 . G = SigFaxTau f,G,R,BASSIGN ; :: thesis: F1 = F2
for G being set st G in bool S holds
F1 . G = F2 . G

proof

let G be set ; :: thesis: ( G in bool S implies F1 . G = F2 . G )
assume G in bool S ; :: thesis: F1 . G = F2 . G
then reconsider G = G as Subset of ;
F1 . G = SigFaxTau f,G,R,BASSIGN by A6
.= F2 . G by A7 ;
hence F1 . G = F2 . G ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:18; :: thesis: verum