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 A3, Def5;

A5: U1,U2 are_similar by A1, UNIALG_2:13;

then A6: U1,U4 are_similar by A3;

A7: U3,U4 are_similar by A2, UNIALG_2:13;

then A8: [:U1,U3:] = UAStr(# [: the carrier of U1, the carrier of U3:],(Opers (U1,U3)) #) by A6, Def5, UNIALG_2:2;

A9: ( the carrier of U1 is Subset of U2 & the carrier of U3 is Subset of U4 ) by A1, A2, UNIALG_2:def 7;

hence the carrier of [:U1,U3:] is Subset of [:U2,U4:] by A8, A4, ZFMISC_1:96; :: according to UNIALG_2:def 7 :: thesis: for b_{1} being Element of bool the carrier of [:U2,U4:] holds

( not b_{1} = the carrier of [:U1,U3:] or ( the charact of [:U1,U3:] = Opers ([:U2,U4:],b_{1}) & b_{1} 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 (signature U2) by UNIALG_1:def 4, A3;

then A11: ( dom the charact of U4 = Seg (len the charact of U4) & len the charact of U4 = len the charact of U2 ) by FINSEQ_1:def 3, UNIALG_1:def 4;

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 A8, Def4;

len the charact of U1 = len (signature U3) by UNIALG_1:def 4, A14;

then A16: ( dom the charact of U3 = Seg (len the charact of U3) & len the charact of U1 = len the charact of U3 ) by FINSEQ_1:def 3, UNIALG_1:def 4;

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 (signature U2) by UNIALG_1:def 4, A5;

then A20: len the charact of [:U1,U3:] = len (Opers ([:U2,U4:],B)) by A19, A15, UNIALG_1:def 4;

reconsider B3 = the carrier of U3 as non empty Subset of U4 by A2, UNIALG_2:def 7;

A21: B3 is opers_closed by A2, UNIALG_2:def 7;

reconsider B1 = the carrier of U1 as non empty Subset of U2 by A1, UNIALG_2:def 7;

A22: B1 is opers_closed by A1, UNIALG_2:def 7;

A23: [: the carrier of U1, the carrier of U3:] c= [: the carrier of U2, the carrier of U4:] by A9, ZFMISC_1:96;

A24: for o being operation of [:U2,U4:] holds B is_closed_on o

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

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 A3, Def5;

A5: U1,U2 are_similar by A1, UNIALG_2:13;

then A6: U1,U4 are_similar by A3;

A7: U3,U4 are_similar by A2, UNIALG_2:13;

then A8: [:U1,U3:] = UAStr(# [: the carrier of U1, the carrier of U3:],(Opers (U1,U3)) #) by A6, Def5, UNIALG_2:2;

A9: ( the carrier of U1 is Subset of U2 & the carrier of U3 is Subset of U4 ) by A1, A2, UNIALG_2:def 7;

hence the carrier of [:U1,U3:] is Subset of [:U2,U4:] by A8, A4, ZFMISC_1:96; :: according to UNIALG_2:def 7 :: thesis: for b

( not b

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 (signature U2) by UNIALG_1:def 4, A3;

then A11: ( dom the charact of U4 = Seg (len the charact of U4) & len the charact of U4 = len the charact of U2 ) by FINSEQ_1:def 3, UNIALG_1:def 4;

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 A8, Def4;

len the charact of U1 = len (signature U3) by UNIALG_1:def 4, A14;

then A16: ( dom the charact of U3 = Seg (len the charact of U3) & len the charact of U1 = len the charact of U3 ) by FINSEQ_1:def 3, UNIALG_1:def 4;

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 (signature U2) by UNIALG_1:def 4, A5;

then A20: len the charact of [:U1,U3:] = len (Opers ([:U2,U4:],B)) by A19, A15, UNIALG_1:def 4;

reconsider B3 = the carrier of U3 as non empty Subset of U4 by A2, UNIALG_2:def 7;

A21: B3 is opers_closed by A2, UNIALG_2:def 7;

reconsider B1 = the carrier of U1 as non empty Subset of U2 by A1, UNIALG_2:def 7;

A22: B1 is opers_closed by A1, UNIALG_2:def 7;

A23: [: the carrier of U1, the carrier of U3:] c= [: the carrier of U2, the carrier of U4:] by A9, ZFMISC_1:96;

A24: for o being operation of [:U2,U4:] holds B is_closed_on o

proof

A37:
dom the charact of U4 = dom (Opers (U4,B3))
by UNIALG_2:def 6;
let o be operation of [:U2,U4:]; :: thesis: B is_closed_on o

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 A8, A10, FINSEQ_1:def 11;

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 A25, FINSEQ_1:def 3;

then A29: n in dom the charact of U2 by A27, FINSEQ_1:def 3;

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 A3, UNIALG_2:1;

then n in dom the charact of U4 by A28, A27, FINSEQ_1:def 3;

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 A21, Def2;

then A35: o4 . s3 in B3 by A33, A32;

( B1 is_closed_on o2 & len s1 = len s0 ) by A22, Def1;

then A36: o2 . s1 in B1 by A33, A31;

dom [[:o2,o4:]] = (arity o2) -tuples_on [: the carrier of U2, the carrier of U4:] by A31, A32, Def3;

then o . s = [(o2 . (pr1 ss)),(o4 . (pr2 ss))] by A31, A32, A30, A34, Def3;

hence o . s in B by A8, A10, A36, A35, ZFMISC_1:87; :: thesis: verum

end;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 A8, A10, FINSEQ_1:def 11;

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 A25, FINSEQ_1:def 3;

then A29: n in dom the charact of U2 by A27, FINSEQ_1:def 3;

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 A3, UNIALG_2:1;

then n in dom the charact of U4 by A28, A27, FINSEQ_1:def 3;

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 A21, Def2;

then A35: o4 . s3 in B3 by A33, A32;

( B1 is_closed_on o2 & len s1 = len s0 ) by A22, Def1;

then A36: o2 . s1 in B1 by A33, A31;

dom [[:o2,o4:]] = (arity o2) -tuples_on [: the carrier of U2, the carrier of U4:] by A31, A32, Def3;

then o . s = [(o2 . (pr1 ss)),(o4 . (pr2 ss))] by A31, A32, A30, A34, Def3;

hence o . s in B by A8, A10, A36, A35, ZFMISC_1:87; :: thesis: verum

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

hence
( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed )
by A24, A20, FINSEQ_2:9; :: thesis: verum
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 A19, A20, A13, A38, FUNCT_1:def 3;

reconsider o4 = the charact of U4 . n as operation of U4 by A19, A20, A38, A11, A40, FUNCT_1:def 3;

reconsider o24 = the charact of [:U2,U4:] . n as operation of [:U2,U4:] by A18, A20, A38, A17, A40, FUNCT_1:def 3;

A41: o24 = [[:o2,o4:]] by A3, A19, A20, A13, A38, A40, Th5;

reconsider o3 = the charact of U3 . n as operation of U3 by A15, A38, A16, A40, FUNCT_1:def 3;

(Opers (U4,B3)) . n = o4 /. B3 by A19, A20, A38, A11, A37, A40, UNIALG_2:def 6;

then A42: o3 = o4 /. B3 by A2, UNIALG_2:def 7;

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 A15, A12, A38, A40, FUNCT_1:def 3;

(Opers (U2,B1)) . n = o2 /. B1 by A19, A20, A13, A38, A39, A40, UNIALG_2:def 6;

then A44: o1 = o2 /. B1 by A1, UNIALG_2:def 7;

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;

.= [[:o2,o4:]] | ((arity o24) -tuples_on B) by A24, A41, UNIALG_2:def 5

.= [[:(o2 /. B1),(o4 /. B3):]] by A51, A48, A52

.= the charact of [:U1,U3:] . n by A14, A8, A40, A44, A42, Def4 ; :: thesis: verum

end;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 A19, A20, A13, A38, FUNCT_1:def 3;

reconsider o4 = the charact of U4 . n as operation of U4 by A19, A20, A38, A11, A40, FUNCT_1:def 3;

reconsider o24 = the charact of [:U2,U4:] . n as operation of [:U2,U4:] by A18, A20, A38, A17, A40, FUNCT_1:def 3;

A41: o24 = [[:o2,o4:]] by A3, A19, A20, A13, A38, A40, Th5;

reconsider o3 = the charact of U3 . n as operation of U3 by A15, A38, A16, A40, FUNCT_1:def 3;

(Opers (U4,B3)) . n = o4 /. B3 by A19, A20, A38, A11, A37, A40, UNIALG_2:def 6;

then A42: o3 = o4 /. B3 by A2, UNIALG_2:def 7;

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 A15, A12, A38, A40, FUNCT_1:def 3;

(Opers (U2,B1)) . n = o2 /. B1 by A19, A20, A13, A38, A39, A40, UNIALG_2:def 6;

then A44: o1 = o2 /. B1 by A1, UNIALG_2:def 7;

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

thus (Opers ([:U2,U4:],B)) . n =
o24 /. B
by A20, A38, A17, A40, UNIALG_2:def 6
[[:(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 A4, XBOOLE_1:1;

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 A48, A54, A55, FUNCT_1:47

.= [(o2 . (pr1 s0)),(o4 . (pr2 s0))] by A43, A47, A48, A54, A55, A53, Def3 ;

reconsider s1 = s as FinSequence of [:B1,B3:] by A8, A10;

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 A43, A47, A56;

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 A49, UNIALG_2:def 5

.= [(o2 . (pr1 s1)),((o4 /. B3) . (pr2 s1))] by A58, A61, FUNCT_1:47

.= [(o2 . (pr1 s1)),((o4 | ((arity o4) -tuples_on B3)) . (pr2 s1))] by A45, UNIALG_2:def 5

.= [(o2 . (pr1 s1)),(o4 . (pr2 s1))] by A59, A60, FUNCT_1:47 ;

hence [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x by A57; :: thesis: verum

end;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 A4, XBOOLE_1:1;

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 A48, A54, A55, FUNCT_1:47

.= [(o2 . (pr1 s0)),(o4 . (pr2 s0))] by A43, A47, A48, A54, A55, A53, Def3 ;

reconsider s1 = s as FinSequence of [:B1,B3:] by A8, A10;

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 A43, A47, A56;

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 A49, UNIALG_2:def 5

.= [(o2 . (pr1 s1)),((o4 /. B3) . (pr2 s1))] by A58, A61, FUNCT_1:47

.= [(o2 . (pr1 s1)),((o4 | ((arity o4) -tuples_on B3)) . (pr2 s1))] by A45, UNIALG_2:def 5

.= [(o2 . (pr1 s1)),(o4 . (pr2 s1))] by A59, A60, FUNCT_1:47 ;

hence [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x by A57; :: thesis: verum

.= [[:o2,o4:]] | ((arity o24) -tuples_on B) by A24, A41, UNIALG_2:def 5

.= [[:(o2 /. B1),(o4 /. B3):]] by A51, A48, A52

.= the charact of [:U1,U3:] . n by A14, A8, A40, A44, A42, Def4 ; :: thesis: verum