let F1, F2 be V230() Function of (bool S),(bool S); :: thesis: ( ( for G being Subset of S holds F1 . G = SigFaxTau (f,G,R,BASSIGN) ) & ( for G being Subset of S holds F2 . G = SigFaxTau (f,G,R,BASSIGN) ) implies F1 = F2 )
assume that
A6: for G being Subset of S holds F1 . G = SigFaxTau (f,G,R,BASSIGN) and
A7: for G being Subset of S holds F2 . G = SigFaxTau (f,G,R,BASSIGN) ; :: thesis: F1 = F2
for G being object st G in bool S holds
F1 . G = F2 . G
proof
let G be object ; :: 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 S ;
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:12; :: thesis: verum