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

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

hence
F1 = F2
by FUNCT_2:12; :: thesis: verum
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;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