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 H₁( Element of Fin (PFuncs (V,C))) -> Element of SubstitutionSet (V,C) = mi $1;
A1: FinUnion (K,(singleton (PFuncs (V,C)))) c= mi (FinUnion (K,(singleton (PFuncs (V,C)))))

proof

let a be object ; :: 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))))) )
reconsider aa = a as set by TARSKI:1;
assume A2: 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
A3: b in K and
A4: a in (singleton (PFuncs (V,C))) . b by SETWISEO:57;
A5: a = b by A4, SETWISEO:55;

A6: now :: thesis: for s being finite set st s in FinUnion (K,(singleton (PFuncs (V,C)))) & s c= aa holds
s = a

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 A7: 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= aa implies s = a )
assume that
A8: s in FinUnion (K,(singleton (PFuncs (V,C)))) and
A9: s c= aa ; :: thesis: s = a
consider t being Element of PFuncs (V,C) such that
A10: t in K and
A11: s in (singleton (PFuncs (V,C))) . t by A8, SETWISEO:57;
s = t by A11, SETWISEO:55;
hence s = a by A3, A5, A9, A10, A7; :: thesis: verum

end;

aa is finite by A3, A5, Th1;
hence a in mi (FinUnion (K,(singleton (PFuncs (V,C))))) by A2, A6, SUBSTLAT:7; :: thesis: verum

end;

consider g being Function of (Fin (PFuncs (V,C))),(SubstitutionSet (V,C)) such that
A12: for B being Element of Fin (PFuncs (V,C)) holds g . B = H₁(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;

A13: now :: thesis: for x, y being Element of Fin (PFuncs (V,C)) holds g . (x \/ y) = the L_join of (SubstLatt (V,C)) . ((g . x),(g . y))

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))
A14: g . x = mi x by A12;
A15: g . y = mi y by A12;
thus g . (x \/ y) = mi (x \/ y) by A12
.= 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 A14, A15, SUBSTLAT:def 4 ; :: thesis: verum

end;

A16: now :: thesis: for a being object st a in K holds
((g * (singleton (PFuncs (V,C)))) | K) . a = ((Atom (V,C)) | K) . a

let a be object ; :: thesis: ( a in K implies ((g * (singleton (PFuncs (V,C)))) | K) . a = ((Atom (V,C)) | K) . a )
assume A17: 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;
A18: a9 is finite by A17, Th1;
then reconsider KL = {a9} as Element of SubstitutionSet (V,C) by Th2;
thus ((g * (singleton (PFuncs (V,C)))) | K) . a = (g * (singleton (PFuncs (V,C)))) . a by A17, FUNCT_1:49
.= g . ((singleton (PFuncs (V,C))) . a9) by FUNCT_2:15
.= g . {a} by SETWISEO:54
.= mi KL by A12
.= KL by SUBSTLAT:11
.= (Atom (V,C)) . a9 by A18, Lm7
.= ((Atom (V,C)) | K) . a by A17, FUNCT_1:49 ; :: thesis: verum

end;

A19: mi (FinUnion (K,(singleton (PFuncs (V,C))))) c= FinUnion (K,(singleton (PFuncs (V,C)))) by SUBSTLAT:8;
A20: rng (singleton (PFuncs (V,C))) c= Fin (PFuncs (V,C)) ;
A21: K c= PFuncs (V,C) by FINSUB_1:def 5;
then K c= dom (Atom (V,C)) by FUNCT_2:def 1;
then A22: 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)) ;
A23: g . ({}. (PFuncs (V,C))) = mi ({}. (PFuncs (V,C))) by A12
.= {} 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 A24: dom (g * (singleton (PFuncs (V,C)))) = dom (singleton (PFuncs (V,C))) by A20, 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 A21, A24, RELAT_1:62;
hence FinJoin (K,(Atom (V,C))) = FinJoin (K,gs) by A22, A16, 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 A23, A13, SETWISEO:53
.= mi (FinUnion (K,(singleton (PFuncs (V,C))))) by A12
.= FinUnion (K,(singleton (PFuncs (V,C)))) by A19, A1 ;
:: thesis: verum