let V be set ; :: thesis: for C being finite set
for K being Element of SubstitutionSet (V,C) holds FinJoin (K,(Atom (V,C))) = FinUnion (K,(singleton (PFuncs (V,C))))
let C be finite set ; :: thesis: for K being Element of SubstitutionSet (V,C) holds FinJoin (K,(Atom (V,C))) = FinUnion (K,(singleton (PFuncs (V,C))))
let K be Element of SubstitutionSet (V,C); :: thesis: FinJoin (K,(Atom (V,C))) = FinUnion (K,(singleton (PFuncs (V,C))))
deffunc H1( Element of Fin (PFuncs (V,C))) -> Element of SubstitutionSet (V,C) = mi $1;
A3: FinUnion (K,(singleton (PFuncs (V,C)))) c= mi (FinUnion (K,(singleton (PFuncs (V,C)))))
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in FinUnion (K,(singleton (PFuncs (V,C)))) or a in mi (FinUnion (K,(singleton (PFuncs (V,C))))) )
assume A4: a in FinUnion (K,(singleton (PFuncs (V,C)))) ; :: thesis: a in mi (FinUnion (K,(singleton (PFuncs (V,C)))))
then consider b being Element of PFuncs (V,C) such that
A5: b in K and
A6: a in (singleton (PFuncs (V,C))) . b by SETWISEO:57;
A7: a = b by A6, SETWISEO:55;
A8: now
K in SubstitutionSet (V,C) ;
then K in { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } by SUBSTLAT:def 1;
then A9: ex AA being Element of Fin (PFuncs (V,C)) st
( K = AA & ( for u being set st u in AA holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in AA & t in AA & s c= t holds
s = t ) ) ;
let s be finite set ; :: thesis: ( s in FinUnion (K,(singleton (PFuncs (V,C)))) & s c= a implies s = a )
assume that
A10: s in FinUnion (K,(singleton (PFuncs (V,C)))) and
A11: s c= a ; :: thesis: s = a
consider t being Element of PFuncs (V,C) such that
A12: t in K and
A13: s in (singleton (PFuncs (V,C))) . t by A10, SETWISEO:57;
s = t by A13, SETWISEO:55;
hence s = a by A5, A7, A11, A12, A9; :: thesis: verum
end;
a is finite by A5, A7, Th2;
hence a in mi (FinUnion (K,(singleton (PFuncs (V,C))))) by A4, A8, SUBSTLAT:7; :: thesis: verum
end;
consider g being Function of (Fin (PFuncs (V,C))),(SubstitutionSet (V,C)) such that
A14: for B being Element of Fin (PFuncs (V,C)) holds g . B = H1(B) from FUNCT_2:sch 4();
 reconsider g = g as Function of (Fin (PFuncs (V,C))), the carrier of (SubstLatt (V,C)) by SUBSTLAT:def 4;
A16: now
let x, y be Element of Fin (PFuncs (V,C)); :: thesis: g . (x \/ y) = the L_join of (SubstLatt (V,C)) . ((g . x),(g . y))
A17: g . x = mi x by A14;
A18: g . y = mi y by A14;
thus g . (x \/ y) = mi (x \/ y) by A14
.= mi ((mi x) \/ y) by SUBSTLAT:13
.= mi ((mi x) \/ (mi y)) by SUBSTLAT:13
.= the L_join of (SubstLatt (V,C)) . ((g . x),(g . y)) by A17, A18, SUBSTLAT:def 4 ; :: thesis: verum
end;
A19: now
let a be set ; :: thesis: ( a in K implies ((g * (singleton (PFuncs (V,C)))) | K) . a = ((Atom (V,C)) | K) . a )
assume A20: a in K ; :: thesis: ((g * (singleton (PFuncs (V,C)))) | K) . a = ((Atom (V,C)) | K) . a
then reconsider a9 = a as Element of PFuncs (V,C) by SETWISEO:9;
A21: a9 is finite by A20, Th2;
then reconsider KL = {a9} as Element of SubstitutionSet (V,C) by Th6;
thus ((g * (singleton (PFuncs (V,C)))) | K) . a = (g * (singleton (PFuncs (V,C)))) . a by A20, FUNCT_1:49
.= g . ((singleton (PFuncs (V,C))) . a9) by FUNCT_2:15
.= g . {a} by SETWISEO:54
.= mi KL by A14
.= KL by SUBSTLAT:11
.= (Atom (V,C)) . a9 by A21, Lm7
.= ((Atom (V,C)) | K) . a by A20, FUNCT_1:49 ; :: thesis: verum
end;
A22: mi (FinUnion (K,(singleton (PFuncs (V,C))))) c= FinUnion (K,(singleton (PFuncs (V,C)))) by SUBSTLAT:8;
A23: rng (singleton (PFuncs (V,C))) c= Fin (PFuncs (V,C)) ;
A24: K c= PFuncs (V,C) by FINSUB_1:def 5;
then K c= dom (Atom (V,C)) by FUNCT_2:def 1;
then A25: dom ((Atom (V,C)) | K) = K by RELAT_1:62;
reconsider gs = g * (singleton (PFuncs (V,C))) as Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) ;
A26: g . ({}. (PFuncs (V,C))) = mi ({}. (PFuncs (V,C))) by A14
.= {} by SUBSTLAT:9
.= Bottom (SubstLatt (V,C)) by SUBSTLAT:26
.= the_unity_wrt the L_join of (SubstLatt (V,C)) by LATTICE2:18 ;
dom g = Fin (PFuncs (V,C)) by FUNCT_2:def 1;
then A27: dom (g * (singleton (PFuncs (V,C)))) = dom (singleton (PFuncs (V,C))) by A23, RELAT_1:27;
dom (singleton (PFuncs (V,C))) = PFuncs (V,C) by FUNCT_2:def 1;
then dom ((g * (singleton (PFuncs (V,C)))) | K) = K by A24, A27, RELAT_1:62;
hence FinJoin (K,(Atom (V,C))) = FinJoin (K,gs) by A25, A19, FUNCT_1:2, LATTICE2:53
.= the L_join of (SubstLatt (V,C)) $$ (K,gs) by LATTICE2:def 3
.= g . (FinUnion (K,(singleton (PFuncs (V,C))))) by A26, A16, SETWISEO:53
.= mi (FinUnion (K,(singleton (PFuncs (V,C))))) by A14
.= FinUnion (K,(singleton (PFuncs (V,C)))) by A22, A3, XBOOLE_0:def 10 ;
:: thesis: verum