let U1, U2, U3, U4 be Universal_Algebra; :: thesis: ( U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar implies [:U1,U3:] is SubAlgebra of [:U2,U4:] )
assume that
A1: U1 is SubAlgebra of U2 and
A2: U3 is SubAlgebra of U4 and
A3: U2,U4 are_similar ; :: thesis: [:U1,U3:] is SubAlgebra of [:U2,U4:]
A4: [:U2,U4:] = UAStr(# [: the carrier of U2, the carrier of U4:],(Opers (U2,U4)) #) by ;
A5: U1,U2 are_similar by ;
then A6: U1,U4 are_similar by A3;
A7: U3,U4 are_similar by ;
then A8: [:U1,U3:] = UAStr(# [: the carrier of U1, the carrier of U3:],(Opers (U1,U3)) #) by ;
A9: ( the carrier of U1 is Subset of U2 & the carrier of U3 is Subset of U4 ) by ;
hence the carrier of [:U1,U3:] is Subset of [:U2,U4:] by ; :: according to UNIALG_2:def 7 :: thesis: for b1 being Element of bool the carrier of [:U2,U4:] holds
( not b1 = the carrier of [:U1,U3:] or ( the charact of [:U1,U3:] = Opers ([:U2,U4:],b1) & b1 is opers_closed ) )

let B be non empty Subset of [:U2,U4:]; :: thesis: ( not B = the carrier of [:U1,U3:] or ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed ) )
assume A10: B = the carrier of [:U1,U3:] ; :: thesis: ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed )
len the charact of U4 = len () by ;
then A11: ( dom the charact of U4 = Seg (len the charact of U4) & len the charact of U4 = len the charact of U2 ) by ;
A12: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def 3;
A13: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def 3;
A14: U1,U3 are_similar by A7, A6;
then A15: len the charact of [:U1,U3:] = len the charact of U1 by ;
len the charact of U1 = len () by ;
then A16: ( dom the charact of U3 = Seg (len the charact of U3) & len the charact of U1 = len the charact of U3 ) by ;
A17: dom (Opers ([:U2,U4:],B)) = Seg (len (Opers ([:U2,U4:],B))) by FINSEQ_1:def 3;
A18: dom the charact of [:U2,U4:] = dom (Opers ([:U2,U4:],B)) by UNIALG_2:def 6;
then len the charact of [:U2,U4:] = len (Opers ([:U2,U4:],B)) by FINSEQ_3:29;
then A19: len the charact of U2 = len (Opers ([:U2,U4:],B)) by A3, A4, Def4;
len the charact of U1 = len () by ;
then A20: len the charact of [:U1,U3:] = len (Opers ([:U2,U4:],B)) by ;
reconsider B3 = the carrier of U3 as non empty Subset of U4 by ;
A21: B3 is opers_closed by ;
reconsider B1 = the carrier of U1 as non empty Subset of U2 by ;
A22: B1 is opers_closed by ;
A23: [: the carrier of U1, the carrier of U3:] c= [: the carrier of U2, the carrier of U4:] by ;
A24: for o being operation of [:U2,U4:] holds B is_closed_on o
proof
let o be operation of [:U2,U4:]; :: thesis:
let s be FinSequence of B; :: according to UNIALG_2:def 3 :: thesis: ( not len s = arity o or o . s in B )
reconsider s0 = s as Element of [: the carrier of U1, the carrier of U3:] * by ;
consider n being Nat such that
A25: n in dom the charact of [:U2,U4:] and
A26: the charact of [:U2,U4:] . n = o by FINSEQ_2:10;
reconsider s3 = pr2 s0 as Element of B3 * by FINSEQ_1:def 11;
reconsider s1 = pr1 s0 as Element of B1 * by FINSEQ_1:def 11;
A27: len the charact of [:U2,U4:] = len the charact of U2 by A3, A4, Def4;
A28: n in Seg (len the charact of [:U2,U4:]) by ;
then A29: n in dom the charact of U2 by ;
then reconsider o2 = the charact of U2 . n as operation of U2 by FUNCT_1:def 3;
len the charact of U4 = len the charact of U2 by ;
then n in dom the charact of U4 by ;
then reconsider o4 = the charact of U4 . n as operation of U4 by FUNCT_1:def 3;
A30: o = [[:o2,o4:]] by A3, A26, A29, Th5;
o4 = the charact of U4 . n ;
then A31: arity o = arity o2 by A3, A26, A29, Th5;
rng s0 c= [: the carrier of U1, the carrier of U3:] by FINSEQ_1:def 4;
then rng s0 c= [: the carrier of U2, the carrier of U4:] by A23;
then s0 is FinSequence of [: the carrier of U2, the carrier of U4:] by FINSEQ_1:def 4;
then reconsider ss = s0 as Element of [: the carrier of U2, the carrier of U4:] * by FINSEQ_1:def 11;
o2 = the charact of U2 . n ;
then A32: arity o = arity o4 by A3, A26, A29, Th5;
assume A33: len s = arity o ; :: thesis: o . s in B
then A34: ss in { w where w is Element of [: the carrier of U2, the carrier of U4:] * : len w = arity o2 } by A31;
( B3 is_closed_on o4 & len s3 = len s0 ) by ;
then A35: o4 . s3 in B3 by ;
( B1 is_closed_on o2 & len s1 = len s0 ) by ;
then A36: o2 . s1 in B1 by ;
dom [[:o2,o4:]] = (arity o2) -tuples_on [: the carrier of U2, the carrier of U4:] by ;
then o . s = [(o2 . (pr1 ss)),(o4 . (pr2 ss))] by A31, A32, A30, A34, Def3;
hence o . s in B by ; :: thesis: verum
end;
A37: dom the charact of U4 = dom (Opers (U4,B3)) by UNIALG_2:def 6;
A38: dom the charact of [:U1,U3:] = Seg (len the charact of [:U1,U3:]) by FINSEQ_1:def 3;
A39: dom the charact of U2 = dom (Opers (U2,B1)) by UNIALG_2:def 6;
for n being Nat st n in dom the charact of [:U1,U3:] holds
the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n
proof
let n be Nat; :: thesis: ( n in dom the charact of [:U1,U3:] implies the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n )
assume A40: n in dom the charact of [:U1,U3:] ; :: thesis: the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n
then reconsider o2 = the charact of U2 . n as operation of U2 by ;
reconsider o4 = the charact of U4 . n as operation of U4 by ;
reconsider o24 = the charact of [:U2,U4:] . n as operation of [:U2,U4:] by ;
A41: o24 = [[:o2,o4:]] by A3, A19, A20, A13, A38, A40, Th5;
reconsider o3 = the charact of U3 . n as operation of U3 by ;
(Opers (U4,B3)) . n = o4 /. B3 by ;
then A42: o3 = o4 /. B3 by ;
o2 = the charact of U2 . n ;
then A43: arity o24 = arity o4 by A3, A19, A20, A13, A38, A40, Th5;
reconsider o1 = the charact of U1 . n as operation of U1 by ;
(Opers (U2,B1)) . n = o2 /. B1 by ;
then A44: o1 = o2 /. B1 by ;
A45: B3 is_closed_on o4 by A21;
then A46: arity (o4 /. B3) = arity o4 by UNIALG_2:5;
o4 = the charact of U4 . n ;
then A47: arity o24 = arity o2 by A3, A19, A20, A13, A38, A40, Th5;
then A48: dom ([[:o2,o4:]] | ((arity o24) -tuples_on B)) = (dom [[:o2,o4:]]) /\ ((arity o2) -tuples_on B) by RELAT_1:61
.= ((arity o2) -tuples_on the carrier of [:U2,U4:]) /\ ((arity o2) -tuples_on B) by A4, A43, A47, Def3
.= (arity o2) -tuples_on B by MARGREL1:21 ;
A49: B1 is_closed_on o2 by A22;
then A50: arity (o2 /. B1) = arity o2 by UNIALG_2:5;
then A51: dom [[:(o2 /. B1),(o4 /. B3):]] = (arity o2) -tuples_on B by A8, A10, A43, A47, A46, Def3;
A52: now :: thesis: for x being object st x in (arity o2) -tuples_on B holds
[[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x
let x be object ; :: thesis: ( x in (arity o2) -tuples_on B implies [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x )
A53: dom ([[:o2,o4:]] | ((arity o24) -tuples_on B)) c= dom [[:o2,o4:]] by RELAT_1:60;
assume A54: x in (arity o2) -tuples_on B ; :: thesis: [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x
then consider s being Element of B * such that
A55: s = x and
A56: len s = arity o2 ;
rng s c= B by FINSEQ_1:def 4;
then rng s c= [: the carrier of U2, the carrier of U4:] by ;
then reconsider s0 = s as FinSequence of [: the carrier of U2, the carrier of U4:] by FINSEQ_1:def 4;
A57: ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x = [[:o2,o4:]] . s0 by
.= [(o2 . (pr1 s0)),(o4 . (pr2 s0))] by A43, A47, A48, A54, A55, A53, Def3 ;
reconsider s1 = s as FinSequence of [:B1,B3:] by ;
reconsider s11 = pr1 s1 as Element of B1 * by FINSEQ_1:def 11;
len (pr1 s1) = len s1 by Def1;
then A58: s11 in { a where a is Element of B1 * : len a = arity o2 } by A56;
reconsider s12 = pr2 s1 as Element of B3 * by FINSEQ_1:def 11;
len (pr2 s1) = len s1 by Def2;
then A59: s12 in { b where b is Element of B3 * : len b = arity o4 } by ;
A60: dom (o4 | ((arity o4) -tuples_on B3)) = (dom o4) /\ ((arity o4) -tuples_on B3) by RELAT_1:61
.= ((arity o4) -tuples_on the carrier of U4) /\ ((arity o4) -tuples_on B3) by MARGREL1:22
.= (arity o4) -tuples_on B3 by MARGREL1:21 ;
A61: dom (o2 | ((arity o2) -tuples_on B1)) = (dom o2) /\ ((arity o2) -tuples_on B1) by RELAT_1:61
.= ((arity o2) -tuples_on the carrier of U2) /\ ((arity o2) -tuples_on B1) by MARGREL1:22
.= (arity o2) -tuples_on B1 by MARGREL1:21 ;
[[:(o2 /. B1),(o4 /. B3):]] . x = [((o2 /. B1) . (pr1 s1)),((o4 /. B3) . (pr2 s1))] by A43, A47, A50, A46, A51, A54, A55, Def3
.= [((o2 | ((arity o2) -tuples_on B1)) . s11),((o4 /. B3) . (pr2 s1))] by
.= [(o2 . (pr1 s1)),((o4 /. B3) . (pr2 s1))] by
.= [(o2 . (pr1 s1)),((o4 | ((arity o4) -tuples_on B3)) . (pr2 s1))] by
.= [(o2 . (pr1 s1)),(o4 . (pr2 s1))] by ;
hence [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x by A57; :: thesis: verum
end;
thus (Opers ([:U2,U4:],B)) . n = o24 /. B by
.= [[:o2,o4:]] | ((arity o24) -tuples_on B) by
.= [[:(o2 /. B1),(o4 /. B3):]] by
.= the charact of [:U1,U3:] . n by A14, A8, A40, A44, A42, Def4 ; :: thesis: verum
end;
hence ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed ) by ; :: thesis: verum