let F1, F2 be Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02); :: thesis: ( ( for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
F1 . U1 = GenUnivAlg H ) & ( for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
F2 . U1 = GenUnivAlg H ) implies F1 = F2 )
assume that
A5: for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
F1 . U1 = GenUnivAlg H and
A6: for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
F2 . U1 = GenUnivAlg H ; :: thesis: F1 = F2
for l being object st l in the carrier of (UnSubAlLattice U01) holds
F1 . l = F2 . l
proof
let l be object ; :: thesis: ( l in the carrier of (UnSubAlLattice U01) implies F1 . l = F2 . l )
assume l in the carrier of (UnSubAlLattice U01) ; :: thesis: F1 . l = F2 . l
then consider U1 being strict SubAlgebra of U01 such that
A7: U1 = l by Th1;
consider H being Subset of U02 such that
A8: H = F .: the carrier of U1 ;
F1 . l = GenUnivAlg H by A5, A7, A8;
hence F1 . l = F2 . l by A6, A7, A8; :: thesis: verum
end;
hence F1 = F2 by FUNCT_2:12; :: thesis: verum